$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
require 'ext_pr1_v4'

#definieren der nötigen Konstanten:
#sekunden pro minute = 60, minuten pro stunde = 60, Stunden pro Tag = 24
#stunde in sekunden = sekunden pro minute * minuten pro stunde
#tag in sekunden = stunde in sekunden * stunden pro tag

MIN_IN_SEC = 60
HOUR_IN_MIN = 60
DAY_IN_HOUR = 24
HALF_DAY_IN_HOUR = DAY_IN_HOUR/2

HOUR_IN_SEC = MIN_IN_SEC * HOUR_IN_MIN
DAY_IN_SEC = DAY_IN_HOUR * HOUR_IN_SEC
HALF_DAY_IN_SEC = DAY_IN_SEC/2
#arithmetik einer uhr, die mit beliebigen zuständen arbeiten kann
class Object
  def halve?() false end
  def hour24?() false end
  def hour12?() false end
  def min?() false end
  def sec?() false end
  def day_sec?() false end
  def clock?() false end
end

class Integer
  #def halve?() false end definition von Object wird geerbt
  def hour24?() self.int? and self.in?(0...DAY_IN_HOUR) end
  def hour12?() self.int? and self.in?(1..(HALF_DAY_IN_HOUR)) end
  def min?() self.int? and self.in?(0...HOUR_IN_MIN) end
  def sec?() self.int? and self.in?(0...MIN_IN_SEC) end
  def day_sec?() self.int? and self.in?(0...DAY_IN_SEC) end
  def clock?() false end
  def normalize() self % DAY_IN_SEC end
#hilfsfunktion um sekunden in ein array aus hour24, min und sek umzuwandeln
  def hrs_min_sec_from_secs()
  hour = self.divmod(HOUR_IN_SEC)[0]
  min = (self.divmod(HOUR_IN_SEC)[1]).divmod(MIN_IN_SEC)[0]
  sec = (self.divmod(HOUR_IN_SEC)[1]).divmod(MIN_IN_SEC)[1]
  [hour, min, sec]
end

end
class Symbol
  def halve?() self == :AM or self == :PM end
end
  
  #ClockSec als Klasse
#ClockSec ::=  ClockSec[:clock_sec] :: DaySec ::
#0 <= DaySec <= DAY_IN_SEC
class ClockSec

   #CREATION 
  def self.[](*args) check_inv(self.new(*args)) end
  def initialize(day_sec) @day_sec = day_sec end

  #SELECTORS
  def day_sec; @day_sec end

  #clock_day_sec ::= clock :: (Clock12[halve, hour12, min, sec] | Clock24[hour24, min,sec] | ClockSec[day_sec])::
  # clock -> Int :: (test (clock_day_sec(Clock12[:AM,1,1,1] => 1,
  #clock_sec(Clock24[1,1,1]) => 1, clock_day_sec(ClockSec[3661]) => 1
  #clock_sec(3) => Err, clock_sec("a") => Err)

  def clock_day_sec()
    check_pre(( self.clock?))

    (self.to_clocksec()).day_sec
  end

   # clock_hour24 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour24(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_hour24(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_hour24("a") => Err)

  def clock_hour24()
    check_pre(( self.clock?))
    self.to_clock24().hour24
  end

  #clock_hour12 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour12(Clock12[:AM,1,1,1] => 1,
  #clock_hour12(Clock24[1,1,1]) => 1, clock_hour12(ClockSec[3661]) => 1
  #clock_hour12(3) => Err, clock_hour12("a") => Err)

  def clock_hour12()
    check_pre(( self.clock?))
    self.to_clock12().hour12
  end

  #clock_min ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_min(Clock12[:AM,1,1,1] => 1,
  #clock_min(Clock24[1,1,1]) => 1, clock_min(ClockSec[3661]) => 1
  #clock_min(3) => Err, clock_min("a") => Err)

   def clock_min()
    check_pre(( self.clock?))
    self.to_clock12().min
   end

  #clock_halve ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> :AM|:PM :: (test (clock_halve(Clock12[:AM,1,1,1] => :AM,
  #clock_halve(Clock24[1,1,1]) => :AM, clock_halve(ClockSec[3661]) => :AM
  #clock_halve(3) => Err, clock_halve("a") => Err)

   def clock_halve()
    check_pre((self.clock?))
    self.to_clock12().halve
   end

  # clock_sec ::= clock :: Clock12[halve, hour12, min, sec] || Clock24[hour24, min,sec] || ClockSec[day_sec]::
  # clock -> Int :: (test (clock_sec(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_sec(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_sec("a") => Err)

  def clock_sec()
    check_pre(( self.clock?))
    (self.to_clock24()).sec
  end
  
  def invariant?() @day_sec.day_sec? end  

  #TYPEPREDS
  def clock_sec?; true end
  def clock24?; false end
  def clock12?; false end
  def clock?; true end

  # EQUIVALENCES

  #ClockSec#== ::= (,o) :: ClockSec x Clock -> Bool
  #test(ClockSec[1].==(ClockSec[1]) => true,
  #ClockSec[1].==(ClockSec[10]) => false)

  def ==(o)
    o.clock? and (self.day_sec == o.day_sec)
  end

  #CONVERSIONS
  def to_s 
    'ClockSec'+'['+(self.day_sec.to_s)+']'
  end

  #ClockSec zu Clock24 konvertieren
  # ClockSec#clocksec_to_clock24  ::= clock :: Clocksec[day_sec] -> Clock24[hour24, min, sec] ::
  #test(clocksec_to_clock24(ClockSec[43200]) => Clock24[12, 0, 0],
  #clocksec_to_clock24(ClockSec[47593] => Clock24[13, 13, 13],
  #clocksec_to_clock24(ClockSec["a"]) => Err)

  def clocksec_to_clock24()
    check_pre((self.clock_sec?))
    self.day_sec.hrs_min_sec_from_secs()
    Clock24[self.day_sec.hrs_min_sec_from_secs()[0],self.day_sec.hrs_min_sec_from_secs()[1],self.day_sec.hrs_min_sec_from_secs()[2]]
  end

  #ClockSec zu Clock12 konvertieren
  #ClockSec#clocksec_to_clock12  ::= clock :: Clocksec[day_sec] -> Clock12[halve, hour12, min, sec] ::
  #test(clocksec_to_clock12(ClockSec[43200])) => Clock12[:AM,12, 0, 0],
  #clocksec_to_clock12(ClockSec[47593]) => Clock12[:PM, 1, 13, 13],
  #clocksec_to_clock12(ClockSec["a"]) => Err)

  def clocksec_to_clock12()
    check_pre((self.clock_sec?))
    halve = (self.day_sec > HALF_DAY_IN_SEC) ? :PM : :AM
    seconds = halve == :AM ?  self.day_sec : self.day_sec % HALF_DAY_IN_SEC
    Clock12[halve,seconds.hrs_min_sec_from_secs()[0] == 0 ? HALF_DAY_IN_HOUR : seconds.hrs_min_sec_from_secs()[0],seconds.hrs_min_sec_from_secs()[1],seconds.hrs_min_sec_from_secs()[2]]
  end  

  #Konvertierung in beiebige Uhren
  #ClockSec#to_clocksec ::= (clock) :: ClockSec -> ClockSec
  def to_clocksec() self end
  #ClockSec#to_clock24 ::= (clock) :: ClockSec -> Clock24
  def to_clock24() self.clocksec_to_clock24() end
  #ClockSec#to_clock12 ::= (clock) :: ClockSec -> Clock12
  def to_clock12() self.clocksec_to_clock12() end
  #ClockSec#to_clock ::= (value) :: Clock -> ClockSec
  def to_clock(value) value.to_clocksec() end

  #OPERATIONs
  #Addieren von zwei Uhrzeiten in sekunden
  #clock_sec_add ::sec1, sec2 :: ClockSec[day_sec] x ClockSec[day_sec] => ClockSec[Nat]
  #where (sec1 and sec2) >= 0 and (sec1 + sec2) is in (0...DAY_IN_SEC)::
  #(test (clock_sec_add(ClockSec[20], ClockSec[50]) => 70,
  #clock_sec_add(ClockSec[3000], ClockSec[5600]) => 8600,
  #clock_sec_add(ClockSec[30], ClockSec["40"]) => Err,
  #clock_sec_add(ClockSec[-10]) => Err)

  def clock_sec_add(sec2)
    check_pre((self.clock_sec? and
        sec2.clock_sec?
      ))
    sec = self.day_sec + sec2.day_sec
    ClockSec[sec.normalize()]
  end

  #Subtrahieren von zwei Uhrzeiten in sekunden
  #clock_sec_sub ::= sec1 - sec2 ::  ClockSec[day_sec] x ClockSec[day_sec] => ClockSec[Nat]
  # where (day_sec1 and day_sec) >= 0
  #(test (clock_sec_sub(ClockSec[90], ClockSec[20] => 70,
  #clock_sec_sub(ClockSec[10], ClockSec[20]) => ClockSec[86390],
  #clock_sec_sub(ClockSec[30], ClockSec["40"]) => Err,
  #clock_sec_sub(ClockSec[-10]) => Err)

  def clock_sec_sub(sec2)
    check_pre((self.clock_sec? and sec2.clock_sec?))
   sec = self.day_sec - sec2.day_sec

    ClockSec[sec.normalize()]
  end

  #nachfolger einer uhrzeit, angegeben in sekunden
  #clock_sec_succ ::= sec1  ::  ClockSec => ClockSec ::

  #clock_sec_succ(ClockSec[86399]) => 0,
  #clock_sec_succClockSec[0]) => 1,
  #clock_sec_succ(ClockSec["40"]) => Err,

  def clock_sec_succ()
   check_pre((self.clock_sec?))
    self.clock_sec_add(ClockSec[1])
  end

  #vorgänger einer uhrzeit, angegeben in sekunden
  #clock_sec_pred ::= sec1  ::  ClockSec[day_sec] => ClockSec[Nat]
  # where (sec1 ) >= 0 ::
  #(test (clock_sec_pred(ClockSec[90] => 89,
  #clock_sec_pred(ClockSec[0]) => 86399,
  #clock_sec_pred(ClockSec["40"]) => Err,

  def clock_sec_pred() 
    check_pre((self.clock_sec?))
   self.clock_sec_sub(ClockSec[1])
  end

  #ClockSec#clock_add ::= (self, clock) :: ClockSec x (ClockSec|Clock24|Clock12) -> ClockSec
  def clock_add(clock2) self.clock_sec_add(clock2.to_clocksec()) end

  #ClockSec#clock_sub ::= (self, clock) :: ClockSec x (ClockSec|Clock24|Clock12) -> ClockSec
  def clock_sub(clock2) self.clock_sec_sub(clock2.to_clocksec()) end

  #ClockSec#clock_succ ::= (self) :: ClockSec -> ClockSec
  def clock_succ() self.to_clocksec.clock_sec_succ() end

  #ClockSec#clock_pred ::= (self) :: ClockSec -> ClockSec
  def clock_pred() self.clock_sec_pred() end
end
#Clock24 als Klasse
#Clock24 ::=  Clock24[:hour24, :min, :sec] :: hour24, min, sec ::
#0 <= hour24 <= DAY_IN_HOUR,
#0 <= min <= HOUR_IN_MIN,
#0 <= sec <= MIN_IN_SEC

class Clock24
 
   #CREATION 
  def self.[](*args) check_inv(self.new(*args)) end
  def initialize(hour24,min,sec) 
  @hour24 = hour24 
  @min = min 
  @sec = sec end
  
  def invariant?()
    @hour24.hour24? and @min.min? and @sec.sec?
  end
   
 #SELECTORS
 def hour24; @hour24 end
 def min; @min end
 def sec; @sec end
 
 #clock_day_sec ::= clock :: (Clock12[halve, hour12, min, sec] | Clock24[hour24, min,sec] | ClockSec[day_sec])::
  # clock -> Int :: (test (clock_day_sec(Clock12[:AM,1,1,1] => 1,
  #clock_sec(Clock24[1,1,1]) => 1, clock_day_sec(ClockSec[3661]) => 1
  #clock_sec(3) => Err, clock_sec("a") => Err)
  
  def clock_day_sec()
    check_pre(( self.clock?))
    
    (self.to_clocksec()).day_sec
  end
  
   # clock_hour24 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour24(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_hour24(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_hour24("a") => Err)
  
    def clock_hour24()
    check_pre(( self.clock?))
    self.to_clock24().hour24
    end
  
  #clock_hour12 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour12(Clock12[:AM,1,1,1] => 1,
  #clock_hour12(Clock24[1,1,1]) => 1, clock_hour12(ClockSec[3661]) => 1
  #clock_hour12(3) => Err, clock_hour12("a") => Err)
  
      def clock_hour12()
    check_pre(( self.clock?))
    self.to_clock12().hour12
  end
  
      
  #clock_min ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_min(Clock12[:AM,1,1,1] => 1,
  #clock_min(Clock24[1,1,1]) => 1, clock_min(ClockSec[3661]) => 1
  #clock_min(3) => Err, clock_min("a") => Err)
 
   def clock_min()
    check_pre(( self.clock?))
    self.to_clock12().min
  end
  
  #clock_halve ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> :AM|:PM :: (test (clock_halve(Clock12[:AM,1,1,1] => :AM,
  #clock_halve(Clock24[1,1,1]) => :AM, clock_halve(ClockSec[3661]) => :AM
  #clock_halve(3) => Err, clock_halve("a") => Err)
  
      def clock_halve()
    check_pre((self.clock?))
    self.to_clock12().halve
    
  end

  # clock_sec ::= clock :: Clock12[halve, hour12, min, sec] || Clock24[hour24, min,sec] || ClockSec[day_sec]::
  # clock -> Int :: (test (clock_sec(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_sec(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_sec("a") => Err)
  
  def clock_sec()
    check_pre(( self.clock?))
    (self.to_clock24()).sec
  end

  
 #TYPEPREDS
  def clock?; true end
  def clock24?; true end
  def clock12?; false end
  def clock_sec?; false end
  
  #EQUIVALENCES
  #Clock24#== ::= (o) :: Clock24 x Clock -> Bool ::
  #test(Clock24[1,1,1].==(Clock24[1,1,1]) => true,
  #Clock24[1,1,2].==(Clock24[1,1,1]) => false,
  def ==(o)
    o.clock? and (o.hour24 == self.hour24) and (o.min == self.min) and (o.sec == self.sec)
  end

  #CONVERSIONS
  def to_s; 'Clock24'+'['+(self.hour24.to_s)+','+(self.min.to_s)+','+(self.sec.to_s)+']' end
  #Clock24 auf ClockSec konvertieren
#clock24_to_clocksec ::= clock :: Clock24[hour24, min, sec] => ClockSec[day_sec] ::
#test(clock_24_to_clocksec(Clock24[0, 0, 0]) => ClockSec[0],
#clock_24_to_clocksec(Clock24[10, 10, 10]) => ClockSec[36610],
#clock_24_to_clocksec(Clock24[0, 0, "a"]) => Err,
#clock_24_to_clocksec(Clock24[-1, 0, 0]) => Err)
  def clock24_to_clocksec()
  check_pre((self.clock24?))
    ClockSec[(self.hour24 * HOUR_IN_SEC) + (self.min * MIN_IN_SEC) + self.sec]
    
end

#Clock24 zu Clock12 konvertieren
#clock24_to_clock12 ::= clock :: Clock24[hour24, min, sec] -> Clock12[halve, hour12, min, sec] ::
#test (clock24_to_clock12(clock24[11,11,11])) => Clock12[:AM,11,11,11],
#(clock24_to_clock12(Clock24[13,13,13])) => Clock12[:PM,1,13,13],
#(clock24_to_clock12(Clock24[1,1,-1]) => Err,

def clock24_to_clock12()
  check_pre((self.clock24?))
(self.clock24_to_clocksec()).clocksec_to_clock12()
end

#Konvertierung allgemein
#Clock24#to_clocksec ::= self :: Clock24 -> ClockSec
def to_clocksec() self.clock24_to_clocksec() end
#Clock24#to_clocksec ::= self :: Clock24 -> Clock24
def to_clock24() self end
#Clock24#to_clocksec ::= self :: Clock24 -> Clock12
def to_clock12() self.clock24_to_clock12() end
#Clock24#to_clock ::= self, value :: Clock24 x (ClockSec|Clock24|Clock12) ->  Clock24
def to_clock(value) value.to_clock24() end

#Clock24#clock_add ::= (self, clock) :: Clock24 x (ClockSec|Clock24|Clock12) -> Clock24
def clock_add(clock2) self.to_clock((self.to_clocksec()).clock_sec_add(clock2.to_clocksec())) end

#Clock24#clock_sub ::= (self, clock) :: Clock24 x (ClockSec|Clock24|Clock12) -> Clock24
def clock_sub(clock2) self.to_clock((self.to_clocksec()).clock_sec_sub(clock2.to_clocksec())) end

#Clock24#clock_succ ::= (self) :: Clock24 -> Clock24
def clock_succ() (self.to_clocksec.clock_sec_succ()).to_clock24() end

#Clock24#clock_pred ::= (self) :: Clock24 -> Clock24
def clock_pred() (self.to_clocksec.clock_sec_pred()).to_clock24() end

end
#Clock12 als Klasse
#Clock12 ::= Clock12[:halve, :hour12, :min, :sec] :: halve, hour, min, sec ::
#halve = (:AM or :PM),
#0 <= hour12 <= (HALF_DAY_IN_HOUR),
#0 <= min <= HOUR_IN_MIN,
#0 <= sec <= MIN_IN_SEC

class Clock12
  #CREATION
  def self.[](*args) check_inv(self.new(*args)) end
  def initialize(halve, hour12, min, sec)
    @halve = halve
    @hour12 = hour12
    @min = min
    @sec = sec
  end

    def invariant?()
      #halve?(halve)
      halve.halve? and
      #hour12?(hour12)
      hour12.hour12? and
      #min?(min)
      min.min? and
      #sec?(sec)
      sec.sec?
    end

  #SELECTORS
  def halve; @halve end
  def hour12; @hour12 end
  def min; @min end
  def sec; @sec end

  #clock_day_sec ::= clock :: (Clock12[halve, hour12, min, sec] | Clock24[hour24, min,sec] | ClockSec[day_sec])::
    # clock -> Int :: (test (clock_day_sec(Clock12[:AM,1,1,1] => 1,
    #clock_sec(Clock24[1,1,1]) => 1, clock_day_sec(ClockSec[3661]) => 1
    #clock_sec(3) => Err, clock_sec("a") => Err)

    def clock_day_sec()
      check_pre(( self.clock?))

      (self.to_clocksec()).day_sec
    end

     # clock_hour24 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
    # clock -> Int :: (test (clock_hour24(Clock12[:AM,1,1,1] => 1,
    #clock_hour24(Clock24[1,1,1]) => 1, clock_hour24(ClockSec[3661]) => 1
    #clock_hour24(3) => Err, clock_hour24("a") => Err)

      def clock_hour24()
      check_pre(( self.clock?))
      self.to_clock24().hour24
      end

    #clock_hour12 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
    # clock -> Int :: (test (clock_hour12(Clock12[:AM,1,1,1] => 1,
    #clock_hour12(Clock24[1,1,1]) => 1, clock_hour12(ClockSec[3661]) => 1
    #clock_hour12(3) => Err, clock_hour12("a") => Err)

        def clock_hour12()
      check_pre(( self.clock?))
      self.to_clock12().hour12
    end


    #clock_min ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
    # clock -> Int :: (test (clock_min(Clock12[:AM,1,1,1] => 1,
    #clock_min(Clock24[1,1,1]) => 1, clock_min(ClockSec[3661]) => 1
    #clock_min(3) => Err, clock_min("a") => Err)

     def clock_min()
      check_pre(( self.clock?))
      self.to_clock12().min
    end

    #clock_halve ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
    # clock -> :AM|:PM :: (test (clock_halve(Clock12[:AM,1,1,1] => :AM,
    #clock_halve(Clock24[1,1,1]) => :AM, clock_halve(ClockSec[3661]) => :AM
    #clock_halve(3) => Err, clock_halve("a") => Err)

        def clock_halve()
      check_pre((self.clock?))
      self.to_clock12().halve

    end

    # clock_sec ::= clock :: Clock12[halve, hour12, min, sec] || Clock24[hour24, min,sec] || ClockSec[day_sec]::
    # clock -> Int :: (test (clock_sec(Clock12[:AM,1,1,1] => 1,
    #clock_hour24(Clock24[1,1,1]) => 1, clock_sec(ClockSec[3661]) => 1
    #clock_hour24(3) => Err, clock_sec("a") => Err)

    def clock_sec()
      check_pre(( self.clock?))
      (self.to_clock24()).sec
    end

  #TYPEPREDS

    def clock?; true end
    def clock12?; true end
    def clock24?; false end
    def clock_sec?; false end
  #Clock12 auf ClockSec konvertieren
  #clock12_to_clocksec ::= clock :: Clock12[halve, hour12, min, sec] => ClockSec[day_sec] ::
  #test
  #(clock_12_to_clocksec(Clock12[:AM, 12, 0, 0]) => ClockSec[0], 
  #clock_12_to_clocksec(Clock12[:PM, 12, 0, 0]) => ClockSec[43200],
  #clock_12_to_clocksec(Clock12[0, 0, "a"]) => Err,)

  #EQUIVALENCES
  def ==(o)
    o.clock? and (o.halve == self.halve) and (o.hour12 == self.hour12) and (o.min == self.min) and (o.sec == self.sec)
  end
  #CONVERSIONS
  def to_s()
    'Clock12'+'['+(self.halve.to_s)+','+(self.hour12.to_s)+','+(self.min.to_s)+','+(self.sec.to_s)+']'
  end
  def clock12_to_clocksec()
    check_pre((self.clock12?))
    sec = (((self.halve == :AM ? 0 : 12) * HOUR_IN_SEC) +
        ((self.hour12 == 12) ? 0 : (self.hour12 * HOUR_IN_SEC)) + 
        (self.min * MIN_IN_SEC) + self.sec)
      ClockSec[sec.normalize()]
  end

  #Clock12 zu Clock24 konvertieren
  #clock12_to_clock24 ::= clock :: Clock12[halve, hour12, min, sec] -> Clock24[hour24, min, sec] ::
  #test (clock12_to_clock24(Clock12[:AM,11,11,11]) => Clock24[11,11,11]),
  #(clock12_to_clock24(Clock12[:PM,1,13,13]) => Clock24[13,13,13],
  #(clock24_to_clock12(Clock12[:AM,1,1,-1]) => Err)

  def clock12_to_clock24()
    check_pre((self.clock12?))
    (self.clock12_to_clocksec()).clocksec_to_clock24()
  end

  #Konvertierung allgemein
#Clock12#to_clocksec ::= self :: Clock12 -> ClockSec
def to_clocksec() self.clock12_to_clocksec() end
#Clock12#to_clock24 ::= self :: Clock12 -> Clock24
def to_clock24() self.clock12_to_clock24 end
#Clock12#to_clock12 ::= self :: Clock12 -> Clock12
def to_clock12()  self end
#Clock12#to_clock ::= self, value :: Clock12 x (ClockSec|Clock24|Clock12) ->  Clock12
  def to_clock(value) value.to_clock12() end

  #OPERATIONS
  #Clock12#clock_add ::= (self, clock) :: Clock12 x (ClockSec|Clock24|Clock12) -> Clock12
  def clock_add(clock2) self.to_clock((self.to_clocksec()).clock_sec_add(clock2.to_clocksec())) end
  #Clock12#clock_sub ::= (self, clock) :: Clock12 x (ClockSec|Clock24|Clock12) -> Clock12
  def clock_sub(clock2) self.to_clock((self.to_clocksec()).clock_sec_sub(clock2.to_clocksec())) end
  #Clock12#clock_succ ::= (self) :: Clock12 -> Clock12
  def clock_succ() (self.to_clocksec.clock_sec_succ()).to_clock12() end
  #Clock12#clock_pred ::= (self) :: Clock12 -> Clock12
  def clock_pred() (self.to_clocksec.clock_sec_pred()).to_clock12() end
end



#to_clock24
#Konvertierung in eine 24 stunden-Uhr
#to_clock24 ::= clock :: Clock12 or ClockSec 
#-> Clock24[hour24, min, sec]
#test (to_clock24(ClockSec[43200]) => Clock24[12, 0, 0],
#to_clock24(ClockSec[47593] => Clock24[13, 13, 13], 
#(to_clock24(Clock12[:AM,11,11,11]) => Clock24[11,11,11]),
#(to_clock24(Clock12[:PM,1,13,13]) => Clock24[13,13,13],
#to_clock24(200) => Err,
#to_clock24("a") => Err



#to_clock12
#Konvertierung in eine 12 stunden uhr
#to_clock12 ::= clock :: Clock24[hour24, min, sec] or ClockSec[day_sec]
#-> Clock12[halve, hour12, min, sec]
#test(to_clock12((ClockSec[43200])) => Clock12[:AM,12, 0, 0],
#(to_clock12(ClockSec[47593])) => Clock12[:PM, 1, 13, 13],
#(to_clock12(clock24[11,11,11])) => Clock12[:AM,11,11,11],
#(to_clock12(Clock24[13,13,13])) => Clock12[:PM,1,13,13],
#to_clock24(200) => Err,
#to_clock24("a") => Err


#to_clock
#beliebige konversion von uhren
#to_clock ::= clock1, clock2 :: Clock x Clock -> Clock ::
#test(to_clock(Clock24[6,6,6], ClockSec[43200]) => Clock24[12,0,0],
#to_clock(Clock24[12,3,1], Clock12[:PM,12,0,0]) => Clock24[12,0,0],
#to_clock(ClockSec[10000], Clock12[:AM, 12,12,12]) => ClockSec[732],
#to_clock(ClockSec[10000], Clock24[12,0,0]) => ClockSec[43200],
#to_clock(Clock12[:PM, 1,1,1], clock24[0,0,0]) => Clock12[:AM, 12,0,0]
#to_clock(Clock12[:PM,1,1,1], clocksec[0]) => Clock12[:AM, 12,0,0]
#to_clock("a". Clock12[:AM, 12,0,0]) => Err)


  
  #clock_add
  #Addieren von zwei Uhrzeiten
  #clock_add ::= clock1, clock2 :: Clock x Clock => Clock ::
  #test(clock_add(ClockSec[3000], ClockSec[5600])) => ClockSec[8600]
  #(clock_add(Clocksec[3000], Clock24[1,1,1])) => ClockSec[6661]
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,1])) => ClockSec[6661]
  #(clock_add(Clock12[:AM,1,1,1], ClockSec[1000])) => Clock12[:AM,1,17,41]
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1])) => Clock12[:AM,2,2,2]
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,1])) => Clock12[:AM,2,2,2]
  #(clock_add(Clock24[1,1,1], ClockSec[1000])) => Clock24[1,17,17]
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,1])) => Clock24[2,2,2]
  #(clock_add(Clock24[1,1,1], Clock24[1,1,1])) => Clock24[2,2,2]
  #exc
  #clock_add(ClockSec["a], ClockSec[5600])) => Err
  #clock_add(ClockSec[3000], ClockSec["a"])) => Err
  #clock_add(ClockSec[-1], ClockSec[5600])) => Err
  #clock_add(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_add(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_add(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_add(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_add(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_add(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_add(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_add(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_add(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  

  #clock_sub
  #Subtrahieren von zwei Uhrzeiten
  #clock_sub ::= clock1, clock2 :: Clock x Clock => Clock ::
  #test(clock_sub(ClockSec[83800], ClockSec[5600])) => ClockSec[8600]
  #(clock_sub(Clocksec[85739], Clock24[1,1,1])) => ClockSec[6661]
  #(clock_sub(Clocksec[85739], Clock12[:AM,1,1,1])) => ClockSec[6661]
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec[1000])) => Clock12[:PM,12,44,45]
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1])) => Clock12[:AM,12,0,0]
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,1])) => Clock12[:AM,12,0,0]
  #(clock_sub(Clock24[1,1,1], ClockSec[1000])) => Clock24[0,44,45]
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,1])) => Clock24[2,2,2]
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,1])) => Clock24[2,2,2]
  #exc
  #clock_sub(ClockSec["a"], ClockSec[5600])) => Err
  #clock_sub(ClockSec[3000], ClockSec["a"])) => Err
  #clock_sub(ClockSec[-1], ClockSec[5600])) => Err
  #clock_sub(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_sub(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_sub(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_sub(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_sub(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_sub(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
#  def clock_sub(clock1,clock2)
#     check_pre(( clock?(clock1) and (clock?(clock2)) ))
#
#    to_clock(clock1, (clock_sec_sub(to_clocksec(clock1), to_clocksec(clock2))))
#  end
  
  
  #clock_succ
  #Nachfolger einer Uhrzeit
  #clock_succ ::= clock1,clock2 :: Clock x Clock => Clock :: 
  #test(clock_succ(ClockSec[1], ClockSec[1]) => Clock24[2]
  #(clock_succ(ClockSec[1], Clock12[:AM,1,1,1]) => ClockSec[3662]
  #(clock_succ(ClockSec[1], Clock24[1,1,1] => [3662]
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec[1]) => Clock12[:AM,1,1,2]
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1]) => Clock12[:AM,1,1,2]
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,1] => Clock12[:AM,1,1,2]
  #(clock_succ(Clock24[1,1,1], ClockSec[1]) => Clock24[1,1,2]
  #(clock_succ(Clock24[1,1,1]), Clock12[:AM,1,1,1] => Clock24[1,1,2]
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,1]) => Clock24[1,1,2]
  #exc
  #clock_succ(ClockSec["a"], ClockSec[5600])) => Err
  #clock_succ(ClockSec[3000], ClockSec["a"])) => Err
  #clock_succ(ClockSec[-1], ClockSec[5600])) => Err
  #clock_succ(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_succ(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_succ(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_succ(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_succ(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_succ(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
#  def clock_succ(clock1,clock2)
#     check_pre(( clock?(clock1) and (clock?(clock2)) ))
#    
#  to_clock(clock1, (clock_sec_succ(to_clocksec(clock2))))
#  end
  
  #clock_pred
  #Vorgänger einer Uhrzeit
  #clock_pred ::= clock1,clock2 :: Clock x Clock => Clock :: 
  #test(clock_pred(ClockSec[2], ClockSec[1]) => Clock24[0]
  #(clock_pred(ClockSec[1], Clock12[:AM,1,1,1]) => ClockSec[3660]
  #(clock_pred(ClockSec[1], Clock24[1,1,1] => [3660]
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec[1]) => Clock12[:AM,1,1,0]
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1]) => Clock12[:AM,1,1,0]
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,1] => Clock12[:AM,1,1,0]
  #(clock_pred(Clock24[1,1,1], ClockSec[1]) => Clock24[1,1,0]
  #(clock_pred(Clock24[1,1,1]), Clock12[:AM,1,1,1] => Clock24[1,1,0]
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,1]) => Clock24[1,1,0]
  #exc
  #clock_pred(ClockSec["a"], ClockSec[5600])) => Err
  #clock_pred(ClockSec[3000], ClockSec["a"])) => Err
  #clock_pred(ClockSec[-1], ClockSec[5600])) => Err
  #clock_pred(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_pred(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_pred(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_pred(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_pred(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_pred(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
#  def clock_pred(clock1,clock2)
#     check_pre(( clock?(clock1) and (clock?(clock2)) ))
#    
#  to_clock(clock1, (clock_sec_pred(to_clocksec(clock2))))
#  end
  
  #allgemeine selektoren
  
  